COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 CLT version of making BMP
C00008 ENDMK
C⊗;
;; CLT version of making BMP
;;  r plisp
;; (load "bmp.mk")
;; (make-thm)
;; save neutp 
;; rename to bmp when checked out

(HERALD MAKE-THM)

(DECLARE (SPECIAL DRIBBLE-FILE))

(DEFUN MAKE-THM NIL

;   A temporary allocation to permit us to load without getting a gc break.

    (ALLOC (QUOTE (SYMBOL (3000. 5000. 256.))))

;   The following two SETQs cause the subsequent LOADs to put their functions
;   and data in "pure" space that won't be garbage collected.

    (SETQ *PURE T)
    (SETQ PURE 1000.)

;   These are the theorem-prover files.

;;     (LOOP FOR ROOT IN (QUOTE (BASIS GENFACT EVENTS CODE-1-A CODE-B-D CODE-E-M
;; 			      CODE-N-R CODE-S-Z IO PPR))
;; 	  DO (APPLY (FUNCTION FASLOAD) (LIST ROOT (QUOTE FASL) (QUOTE THM))))
;;[CLT fix omit 'THM in FASLOAD list]

    (LOOP FOR ROOT IN (QUOTE (BASIS GENFACT EVENTS CODE-1-A CODE-B-D CODE-E-M
			      CODE-N-R CODE-S-Z IO PPR))
	  DO (APPLY (FUNCTION FASLOAD) (LIST ROOT (QUOTE FASL) )))

;   Two files that would get loaded after running the theorem-prover just a
;   little if we did not load them now are:

    (FASLOAD MACAID FASL LISP)
    (FASLOAD SORT FASL LISP)
    (FASLOAD LET FASL LISP)
    
;   We have finished loading the code that we want to have purified.

    (SETQ *PURE NIL PURE NIL)

;   We want the theorem-prover to run as fast as possible usually.  User
;   defined functions in the theory can be interpreted, hence the setting of
;   *RSET.

    (SETQ *RSET NIL NOUUO NIL)

    (GC)

;   This is an empirically derived ALLOCation that barely gets us through the
;   PROVEALLs in XXXS.LISP (with the three SWAPOUTs).

    (ALLOC (QUOTE (LIST (70000. 70000. 0.25) 
		   SYMBOL (3000. 7000. 0.10)
		   FIXNUM (9000. 90000. 0.25))))

;   A dribble file may be open that would prevent the SUSPEND.

    (COND ((BOUNDP (QUOTE DRIBBLE-FILE)) (DRIBBLE-END)))

;   Purify and return to the EXEC.

    (SUSPEND)

;;[CLT omit the groveling for MACLISP directory - at SAIL LISP knows where to look]

    (COND ((FBOUNDP (QUOTE DRIBBLE-START))
	   (DRIBBLE-START)))

;[CLT]setup em-interface
    (COND ((AND (STATUS FEATURES SAIL) SI:ECALLEDP)
	   (SETQ -EM:HERALD- ())
	   (EM:MAIL-INTERFACE-INITIALIZE)))
;   We're back and ready to start up a theorem-prover now.  Perhaps there is a
;   THM.INI file on the home directory of the user; if so, load it.
;;[CLT do crunit hack then probef and load]

;set file default to luser udir
    (APPLY 'CRUNIT (LIST 'DSK (STATUS UDIR)))
;load thm.ini from luser area
    (COND ((PROBEF "THM.INI") (LOAD "THM.INI")))

    (QUOTE *))